COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	comment@ Axioms for extensional forms@
C00006 00003	comment@ Axioms aimed at formalizing individual concepts in the context
C00008 ENDMK
C⊗;
comment@ Axioms for extensional forms@

declare INDCONST V V0 V1 V2 V3 ε variable;
declare INDVAR v v0 v1 v2 v3 ε variable;

declare INDVAR u u0 u1 u2 u3 ε termform;
declare INDVAR p p0 p1 p2 p3 ε boolform;
declare INDVAR e e0 e1 e2 e3 ε environment;
declare INDVAR f f0 f1 f2 f3 ε functionform;
declare INDVAR c c0 c1 c2 c3 ε object;

declare OPCONST value(termform,environment) = termform;
declare PREDCONST true(boolform,environment);
declare OPCONST assign(variable,object,environment) = environment;

declare OPCONST apply(functionform,termform) = termform;
declare OPCONST lambda(variable,termform) = functionform;

axiom lambda:	∀v u1 u2 e.(value(apply(lambda(v,u1),u2),e) = value(u1,
assign(v,value(u2,e),e)));;

MOREGENERAL termform ≥ {object,variable};

axiom object:	∀c e.(value(c,e) = c);;

axiom assign:	∀v c e.(value(v,assign(v,c,e)) = c),
		∀v1 v2 c e.(¬v1=v2 ⊃ value(v1,assign(v2,c,e)) = value(v1,e));;

declare OPCONST all(variable,boolform) = boolform;
declare OPCONST exist(variable,boolform) = boolform;
DECLARE OPCONST and(boolform,boolform) = boolform [L←555,R←550];
DECLARE OPCONST or(boolform,boolform) = boolform [L←535,R←540];
DECLARE OPCONST implies(boolform,boolform) = boolform [L←515,R←520];
DECLARE OPCONST equiv(boolform,boolform) = boolform [L←505,R←510];
DECLARE OPCONST not(boolform) = boolform [R←575];

axiom all:	∀ v p e.(true(all(v,p),e) ≡ ∀c.true(p,assign(v,c,e)));;
axiom exist:	∀ v p e.(true(exist(v,p),e) ≡ ∃c.true(p,assign(v,c,e)));;

axiom and:	∀ p1 p2 e.(true(p1 and p2,e) ≡ true(p1,e) ∧ true(p2,e));;
axiom or:	∀ p1 p2 e.(true(p1 or p2,e) ≡ true(p1,e) ∨ true(p2,e));;
axiom implies:	∀ p1 p2 e.(true(p1 implies p2,e) ≡ (true(p1,e) ⊃ true(p2,e)));;
axiom equiv:	∀ p1 p2 e.(true(p1 equiv p2,e) ≡ (true(p1,e) ≡ true(p2,e)));;
axiom not:	∀p e.(true(not p,e) ≡ ¬true(p,e));;

DECLARE OPCONST equal(termform,termform) = boolform [L←600,R←605];

axiom equal:	∀u1 u2 e.(true(u1 equal u2,e) ≡ (value(u1,e) = value(u2,e)));;

mark foo;
declare OPCONST subst(termform,variable,termform) = termform;
axiom subst:	∀v u.(subst(v,v,u) = u),
		∀v u.(subst(u,v,v) = u),
		∀v1 v2 u.(¬v1=v2 ⊃ subst(u,v1,v2) = v2)
;;
comment@ Axioms aimed at formalizing individual concepts in the context
of my "First order theories of propositions and individual concepts"@

declare PREDCONST nec(boolform)[R←570];
declare INDVAR m m0 m1 m2 m3 ε manform;
declare INDCONST Mike Pat Joe John Mary mike pat joe john mary ε manform;
declare OPCONST telephone(manform) = termform[R←610];

declare OPCONST know(manform,termform) = boolform;
declare OPCONST k(manform,boolform) = boolform;

axiom nec:	∀p.(nec p ≡ ∀e.true(p,e));;

axiom telephone:	∀u e.(value(telephone m,e) = telephone value(m,e));;
			
axiom morsubst:
		∀u v m.(subst(u,v,telephone m) = telephone subst(u,v,m))
		∀m p v u.(subst(u,v,k(m,p)) = k(subst(u,v,m),subst(u,v,p)))
		∀m u1 v u2.(subst(u1,v,know(m,u2))
			 = know(subst(u1,v,m),subst(u1,v,u2)))
;;

axiom know:	∀m1 m2 m e.true(know(m,telephone m1) and k(m,m1 equal m2)
			implies know(m,telephone m2),e)
		∀m u u1 u2.nec(k(m,u1 equal u2) implies
			k(m,subst(u1,v,u) equal subst(u2,v,u)))
		∀m u1 u2.nec(k(m,u1 equal u2) and know(m,u1) implies know(m,u2))
;;